mu(f) == if f(0) 0 else mu(x.f(x+1))+1 fi  (recursive) 

latex

Definitions	if b t else f fi, Y
FDL editor aliases	mu